Integrating Formal Verification into Computer Organization and Architecture Courses,” 17 th Eastern Small College Computing Conference (ESCCC ’01), October 2001

The high complexity of modern hardware and software systems necessitates the use of formal methods for checking the satisfaction of desired properties and the absence of design flaws. Numerous methods have been developed, and some, such as model checking and the ω-automata approach, have found wide acceptance in the computer industry and have led to the development of powerful verification tools. However, the popularity of these methods has not been firmly established in the Computer Science and Engineering curriculum. This paper presents an approach to integrating current verification research results into a typical, small-college Computer Organization and Architecture course. OVERVIEW OF FORMAL VERIFICATION The ever-increasing complexity of hardware and software systems and the protocols which govern their behavior has significantly increased the potential for design errors, and, at the same time, limited the usefulness of the classical simulation and testing methods for uncovering design faults. A powerful alternative, which ha